Nuprl Lemma : l_subset_wf
11,40
postcript
pdf
T
:Type,
as
,
bs
:(
T
List). l_subset(
T
;
as
;
bs
)
latex
Definitions
P
Q
,
l_subset(
T
;
as
;
bs
)
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
l
member
wf
origin
T:Type, as, bs:(T List). l_subset(T;as;bs) 
T:Type, as, bs:(T List). l_subset(T;as;bs) 
Q Tx:A. B(x)